#pragma once

#include "Term.hpp"

namespace terms {
	/**
	 * \brief the base class for the base terms in a term system
	 *
	 * The library supports multiple, independent term systems.
	 * A term system has two fundamental properties:
	 *
	 * - It is an upper lattice with a common BaseTerm
	 * - All terms in the term system form a total order.  
	 *
	 * The base term is created by deriving from the TermSystem class.
	 * The total order is created by making sure that each concrete
	 * term type in the term system has a unique index number and that
	 * terms within a single type have a total order.o
	 * 
	 * For example, in First Order Logic, you can sort predicates first,
	 * forall second, followed by exists, and so on. This way, you only
	 * need to provide proper order for forall terms within themselves,
	 * as they will never need to be compared with other term types.
	 *
	 * The order is often arbitrary but some total order is required.
	 *
	 * \tparam BaseTerm The type of the base term of the term system.
	 *  Ususally the same as the class of the base term.
	 * \tparam TermTypeOrder The type of the term type order. Usually an
	 * enum.
	 *
	 * Typical use
	 * ===========
	 *
	 * \code{.cpp}
	 * enum MyTermOrder {
	 * 	TermTypeA,
	 * 	TermTypeB
	 * };
	 *
	 * class MyBaseTerm
	 * 		: public TermSytem<MyBaseTerm, MyTermOrder>
	 * {
	 * };
	 * \endcode
	 * 
	 **/
	template <typename BaseTerm, typename TermTypeOrder=int>
	class TermSystem
		: public Term
	{
	public:
		typedef TermTypeOrder TypeOrder;

	public:
		/**
		 * \brief Retrieve the type order of the current term.
		 **/
		virtual TermTypeOrder get_type_order() const = 0;

	public:
		virtual bool operator ==(const BaseTerm &other) const = 0;

	public:
		virtual bool operator <(const BaseTerm &other) const = 0;

	public:
		virtual bool operator !=(const BaseTerm &other) const
		{
			return !(*this == other);
		}

	public:
		virtual bool operator <=(const BaseTerm &other) const
		{
			return (*this == other) || (*this < other);
		}

	public:
		virtual bool operator >(const BaseTerm &other) const
		{
			return other < *(dynamic_cast<const BaseTerm * const>(this));
		}

	public:
		virtual bool operator >=(const BaseTerm &other) const
		{
			return (*this == other) || (other < *(dynamic_cast<const BaseTerm * const>(this)));
		}
	};
}
